i, x:Id, a, b:Knd, T:Type.
@i: only members of [a; b] affect x :T  Dsys
& (D:Dsys.
& (@i: only members of [a; b] affect x :T  D
& ( D 
& ( realizes es.
& ( vartype(i;x)  T
& ( & e@i.
& ( & ((x after e) = (x when e)  T  kind(e) = a  Knd  kind(e) = b  Knd)
& ( & & (kind(e) = a  kind(e) = b  Knd  (x after e) = (x when e)  T)) 

latex

Definitions

Case b of inl(x)  s(x) ; inr(y)  t(y), kind(e), kind(e), Knd, left+right, es_info(es), ES(the_w), s = t, t  T, World, x:A. B(x), FairFifo, E, Prop, P  Q, P  Q, x:AB(x), False, A, Type, Void, Dec(P), x when e, (x after e), <a,b>, vartype(i;x), A & B, P & Q, type List, nil, (x  l), P  Q, x:AB(x), P  Q, {T}, car.cdr, loc(e), Id, e@i. P(e), @i only events in L change   x : T, PossibleWorld(D;w), D1  D2, Dsys, D realizes es. P(es)

Lemmas

s-frame-rule, dsys wf, d-sub wf, possible-world wf, Id wf, es-loc wf, es-vartype wf, cons member, implies functionality wrt iff, not functionality wrt iff, or functionality wrt iff, nil member, l member wf, es-after wf, es-when wf, not wf, decidable or, decidable equal Kind, false wf, es-kind wf, es-E wf, w-es wf, fair-fifo wf, world wf, Knd wf